es:ES, i, x:Id, T, A:Type, f:(TA), Lx:Knd List.
es-frame(es;i;Lx;x;T)
 e@i. (kind(e)  Lx)  f((x after e)) = f(x when e)  A
 e@i. f(x when e) = f(x when es-init(es;e)) 

latex

Definitions	es-frame(es;i;L;x;T), ES, t  T, Id, Type, x:AB(x), Knd, type List, x:A. B(x), x when e, vartype(i;x), (x after e), loc(e), s = t, E, {x:A| B(x) }, f(a), x(s), Prop, kind(e), (x  l), P  Q, x. t(x), e@i. P(e), x:AB(x), <a,b>, A & B, left+right, P  Q, Dec(P)
Lemmas	es-vartype wf, decidable l member, decidable equal Kind, es-constant1, alle-at wf, l member wf, es-kind wf, es-E wf, es-loc wf, es-after wf, es-when wf, es-frame wf, Knd wf, Id wf, event system wf